\begin{tabbing}
$\forall$${\it es}$:ES, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $T$:Type, $i$:Id, $f$:(State(${\it ds}$)$\rightarrow$$T$).
\\[0ex]($\forall$$x$, $y$:$T$. Dec($x$ = $y$))
\\[0ex]$\Rightarrow$ @$i$ discrete ${\it ds}$
\\[0ex]$\Rightarrow$ \=$\forall$${\it e'}$@$i$.\+
\\[0ex]($\forall$$e$:E. $e$ $\leq$loc ${\it e'}$  $\Rightarrow$ ($f$((discrete state when $e$)) = $f$((discrete state after ${\it e'}$)) $\in$ $T$))
\\[0ex]$\vee$ ($\exists$\=$e$:E\+
\\[0ex]($e$ $\leq$loc ${\it e'}$ 
\\[0ex]c$\wedge$ \=(($\neg$($f$((discrete state when $e$)) = $f$((discrete state after ${\it e'}$))))\+
\\[0ex]\& (\=$\forall$${\it e''}$:E.\+
\\[0ex]($e$ $<$loc ${\it e''}$)
\\[0ex]$\Rightarrow$ ${\it e''}$ $\leq$loc ${\it e'}$ 
\\[0ex]$\Rightarrow$ ($f$((discrete state when ${\it e''}$)) = $f$((discrete state after ${\it e'}$)) $\in$ $T$)))))
\-\-\-\-
\end{tabbing}